Inference at * 1 1 2 2 
Iof proof for Lemma decidable implies better:



1. P : 
2. Q : x:P.
3. P
4. P  Dec(Q)
5. (P  Q)  
  (P  Q)  ((P  Q)) 

latex

 by OrLeft THEN Auto  

latex

 .

Definitions	P  Q, False, P  Q, , A, x:A. B(x), t  T
Lemmas	not wf